Nuprl Definition : ma-bframe 11,40

M.bframe(k sends on l) == L != (M.2.2.2.2.2.2.2.2.2).1(k deq-member(IdLnkDeq;l;L
latex



clarification:

M.bframe(k sends on l)
== fpf-val(KindDeq; ((M.2.2.2.2.2.2.2.2.2).1); kk,L.(deq-member(IdLnkDeq;l;L))) 
latex


Definitionsz != f(x P(a;z), KindDeq, t.1, t.2, b, deq-member(eq;x;L), IdLnkDeq
FDL editor aliasesma-bframe

origin